es is an event system of D == w:World. p:FairFifo. (PossibleWorld(D;w) & es = ES(w)) 

latex

---

clarification:

d-es{i:l}
d-es(D; es)
== w:world{i:l}
== p:fair-fifo{i:l}(w). (possible-world{i:l}(D; w) & es = w-es{i:l}(w; p)  ES{i}) 

latex

Definitions	World, x:A. B(x), FairFifo, P & Q, PossibleWorld(D;w), s = t, ES, ES(the_w)
FDL editor aliases	d-es